(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
+(x, 0) → x
+(minus(x), x) → 0
minus(0) → 0
minus(minus(x)) → x
minus(+(x, y)) → +(minus(y), minus(x))
*(x, 1) → x
*(x, 0) → 0
*(x, +(y, z)) → +(*(x, y), *(x, z))
*(x, minus(y)) → minus(*(x, y))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
+(z0, 0) → z0
+(minus(z0), z0) → 0
minus(0) → 0
minus(minus(z0)) → z0
minus(+(z0, z1)) → +(minus(z1), minus(z0))
*(z0, 1) → z0
*(z0, 0) → 0
*(z0, +(z1, z2)) → +(*(z0, z1), *(z0, z2))
*(z0, minus(z1)) → minus(*(z0, z1))
Tuples:
MINUS(+(z0, z1)) → c4(+'(minus(z1), minus(z0)), MINUS(z1), MINUS(z0))
*'(z0, +(z1, z2)) → c7(+'(*(z0, z1), *(z0, z2)), *'(z0, z1), *'(z0, z2))
*'(z0, minus(z1)) → c8(MINUS(*(z0, z1)), *'(z0, z1))
S tuples:
MINUS(+(z0, z1)) → c4(+'(minus(z1), minus(z0)), MINUS(z1), MINUS(z0))
*'(z0, +(z1, z2)) → c7(+'(*(z0, z1), *(z0, z2)), *'(z0, z1), *'(z0, z2))
*'(z0, minus(z1)) → c8(MINUS(*(z0, z1)), *'(z0, z1))
K tuples:none
Defined Rule Symbols:
+, minus, *
Defined Pair Symbols:
MINUS, *'
Compound Symbols:
c4, c7, c8
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
MINUS(+(z0, z1)) → c4(+'(minus(z1), minus(z0)), MINUS(z1), MINUS(z0))
*'(z0, +(z1, z2)) → c7(+'(*(z0, z1), *(z0, z2)), *'(z0, z1), *'(z0, z2))
*'(z0, minus(z1)) → c8(MINUS(*(z0, z1)), *'(z0, z1))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
+(z0, 0) → z0
+(minus(z0), z0) → 0
minus(0) → 0
minus(minus(z0)) → z0
minus(+(z0, z1)) → +(minus(z1), minus(z0))
*(z0, 1) → z0
*(z0, 0) → 0
*(z0, +(z1, z2)) → +(*(z0, z1), *(z0, z2))
*(z0, minus(z1)) → minus(*(z0, z1))
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:
+, minus, *
Defined Pair Symbols:none
Compound Symbols:none
(5) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(6) BOUNDS(O(1), O(1))